0 CpxTRS
↳1 DependencyGraphProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxTRS
↳3 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 NarrowingProof (BOTH BOUNDS(ID, ID), 3 ms)
↳10 CpxTypedWeightedCompleteTrs
↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳12 CpxRNTS
↳13 InliningProof (UPPER BOUND(ID), 129 ms)
↳14 CpxRNTS
↳15 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CpxRNTS
↳17 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳18 CpxRNTS
↳19 IntTrsBoundProof (UPPER BOUND(ID), 213 ms)
↳20 CpxRNTS
↳21 IntTrsBoundProof (UPPER BOUND(ID), 26 ms)
↳22 CpxRNTS
↳23 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳24 CpxRNTS
↳25 IntTrsBoundProof (UPPER BOUND(ID), 179 ms)
↳26 CpxRNTS
↳27 IntTrsBoundProof (UPPER BOUND(ID), 49 ms)
↳28 CpxRNTS
↳29 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳30 CpxRNTS
↳31 IntTrsBoundProof (UPPER BOUND(ID), 176 ms)
↳32 CpxRNTS
↳33 IntTrsBoundProof (UPPER BOUND(ID), 30 ms)
↳34 CpxRNTS
↳35 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳36 CpxRNTS
↳37 IntTrsBoundProof (UPPER BOUND(ID), 3397 ms)
↳38 CpxRNTS
↳39 IntTrsBoundProof (UPPER BOUND(ID), 30 ms)
↳40 CpxRNTS
↳41 FinalProof (⇔, 0 ms)
↳42 BOUNDS(1, n^1)
from(X) → cons(X, n__from(n__s(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
from(X) → n__from(X)
s(X) → n__s(X)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(X) → X
sel(0, cons(X, Y)) → X
activate(n__from(X)) → from(activate(X))
from(X) → cons(X, n__from(n__s(X)))
from(X) → n__from(X)
s(X) → n__s(X)
activate(X) → X
activate(n__s(X)) → s(activate(X))
sel(0, cons(X, Y)) → X [1]
activate(n__from(X)) → from(activate(X)) [1]
from(X) → cons(X, n__from(n__s(X))) [1]
from(X) → n__from(X) [1]
s(X) → n__s(X) [1]
activate(X) → X [1]
activate(n__s(X)) → s(activate(X)) [1]
sel(0, cons(X, Y)) → X [1]
activate(n__from(X)) → from(activate(X)) [1]
from(X) → cons(X, n__from(n__s(X))) [1]
from(X) → n__from(X) [1]
s(X) → n__s(X) [1]
activate(X) → X [1]
activate(n__s(X)) → s(activate(X)) [1]
sel :: 0 → cons:n__from:n__s → cons:n__from:n__s 0 :: 0 cons :: cons:n__from:n__s → cons:n__from:n__s → cons:n__from:n__s activate :: cons:n__from:n__s → cons:n__from:n__s n__from :: cons:n__from:n__s → cons:n__from:n__s from :: cons:n__from:n__s → cons:n__from:n__s n__s :: cons:n__from:n__s → cons:n__from:n__s s :: cons:n__from:n__s → cons:n__from:n__s |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
sel
activate
from
s
const
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
const => 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ s(s(activate(X2))) :|: z = 1 + (1 + X2), X2 >= 0
activate(z) -{ 2 }→ s(from(activate(X1))) :|: X1 >= 0, z = 1 + (1 + X1)
activate(z) -{ 2 }→ from(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ from(s(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ from(from(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
from(z) -{ 1 }→ 1 + X + (1 + (1 + X)) :|: X >= 0, z = X
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from(z) -{ 1 }→ 1 + X + (1 + (1 + X)) :|: X >= 0, z = X
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ s(s(activate(X2))) :|: z = 1 + (1 + X2), X2 >= 0
activate(z) -{ 2 }→ s(from(activate(X1))) :|: X1 >= 0, z = 1 + (1 + X1)
activate(z) -{ 2 }→ from(s(activate(X''))) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ from(from(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 3 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z = 1 + X, X >= 0, X' >= 0, X = X'
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
from(z) -{ 1 }→ 1 + X + (1 + (1 + X)) :|: X >= 0, z = X
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
{ from } { sel } { s } { activate } |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: ?, size: O(n1) [3 + 2·z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] sel: runtime: ?, size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] sel: runtime: O(1) [1], size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] sel: runtime: O(1) [1], size: O(n1) [z'] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] sel: runtime: O(1) [1], size: O(n1) [z'] s: runtime: ?, size: O(n1) [1 + z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] sel: runtime: O(1) [1], size: O(n1) [z'] s: runtime: O(1) [1], size: O(n1) [1 + z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] sel: runtime: O(1) [1], size: O(n1) [z'] s: runtime: O(1) [1], size: O(n1) [1 + z] |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] sel: runtime: O(1) [1], size: O(n1) [z'] s: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: ?, size: EXP |
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ s(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ s(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(s(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ from(from(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 3 }→ 1 + X' + (1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 1 }→ 1 + z + (1 + (1 + z)) :|: z >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sel(z, z') -{ 1 }→ X :|: Y >= 0, X >= 0, z' = 1 + X + Y, z = 0
from: runtime: O(1) [1], size: O(n1) [3 + 2·z] sel: runtime: O(1) [1], size: O(n1) [z'] s: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: O(n1) [4 + 4·z], size: EXP |